X, Y:ik:LocKnd fp Top, ik:LocKnd.
interface-union(X;Y)(ik)
~
(s,v. if ik  dom(X)
then if ik  dom(Y)
then then case X(ik)(s,v)
then then of inl(x) => inl inl x  
then then o| inr(x) => case Y(ik)(s,v) of inl(x) => inl (inr x )  | inr(x) => inr x 
then else case X(ik)(s,v) of inl(x) => inl inl x   | inr(x) => inr x 
then fi 
else case Y(ik)(s,v) of inl(x) => inl (inr x )  | inr(x) => inr x 
fi ) 

latex

Definitions	Top, t  T, LocKnd, x:A. B(x), (x  l), {x:A| B(x)} , x:AB(x), type List, x:A  B(x), f(x), interface-union(X;Y), a:A fp B(a)
Lemmas	l member wf, LocKnd wf, top wf